<!DOCTYPE html>
<html lang="en" dir="ltr" class="no-js">
<head>
    <meta charset="utf-8" />
    <title>Workcraft - tutorial:petri_net:start</title>
    <script>(function(H){H.className=H.className.replace(/\bno-js\b/,'js')})(document.documentElement)</script>
    <meta name="generator" content="DokuWiki"/>
<meta name="robots" content="index,follow"/>
<meta name="keywords" content="tutorial,petri net,start"/>
<link rel="search" type="application/opensearchdescription+xml" href="../lib/exe/opensearch.html" title="Workcraft"/>
<link rel="start" href="start.html"/>
<link rel="contents" href="start.html" title="Sitemap"/>
<link rel="alternate" type="application/rss+xml" title="Changes" />
<link rel="alternate" type="application/rss+xml" title="Current namespace" />
<link rel="alternate" type="text/html" title="Plain HTML" href="../_export/xhtml/tutorial/petri_net/start.xhtml"/>
<link rel="alternate" type="text/plain" title="Wiki Markup" href="../_export/raw/tutorial/petri_net/start.raw"/>
<link rel="canonical" href="http://www.workcraft.org/tutorial/petri_net/start"/>
<link rel="stylesheet" type="text/css" href="../lib/exe/css.php.t.dokuwiki-light-export.css"/>
<script type="text/javascript">/*<![CDATA[*/var NS='tutorial:petri_net';var JSINFO = {"id":"tutorial:petri_net:start","namespace":"tutorial:petri_net"};
/*!]]>*/</script>
<script type="text/javascript" charset="utf-8" src="../lib/exe/js.php.t.dokuwiki-light-export.js"></script>
    <meta name="viewport" content="width=device-width,initial-scale=1" />
    <link rel="shortcut icon" href="../favicon.ico" />
<link rel="apple-touch-icon" href="../apple-touch-icon.png" />
    </head>

<body>
    <!--[if lte IE 7 ]><div id="IE7"><![endif]--><!--[if IE 8 ]><div id="IE8"><![endif]-->
    <div id="dokuwiki__site"><div id="dokuwiki__top" class="site dokuwiki mode_show tpl_dokuwiki-light-export     ">

        
<!-- ********** HEADER ********** -->
<div id="dokuwiki__header"><div class="pad group">

        <h1><a href="../start.html"  title="Workcraft start page"><img src="../logo.png" width="327" height="57" alt="" /></a></h1>
    
    <div class="tools group">
        <!-- USER TOOLS -->
                    <div id="dokuwiki__usertools">
                <h3 class="a11y">User Tools</h3>
                <ul>
                    <li><a href="start.html"  class="action login" rel="nofollow" title="Login">Login</a></li>                </ul>
            </div>
        
        <!-- SEARCH TOOLS -->
        <div id="dokuwiki__searchtools">
            <h3 class="a11y"></h3>
            <form action="../start.html" accept-charset="utf-8" class="search" id="dw__search" method="get" role="search"><div class="no"><input type="hidden" name="do" value="search" /><input type="text" id="qsearch__in" accesskey="f" name="id" class="edit" title="[F]" /><input type="submit" value="Search" class="button" title="Search" /><div id="qsearch__out" class="ajax_qsearch JSpopup"></div></div></form>        </div>

        <!-- SITE TOOLS -->
        <div id="dokuwiki__sitetools">
            <h3 class="a11y">Site Tools</h3>
                            <div class="mobileTools">
                    <li><a href="start.html"  class="action login" rel="nofollow" title="Login">Login</a></li>                </div>
                <ul>
                                    </ul>
                    </div>
    </div>

    <!-- BREADCRUMBS -->
    
    
    <hr class="a11y" />
</div></div><!-- /header -->

        <div class="wrapper group">

            
            <!-- ********** CONTENT ********** -->
            <div id="dokuwiki__content"><div class="pad group">
                <div class="pageId"><span>tutorial:petri_net:start</span></div>
                <div class="page group">
                                                            <!-- wikipage start -->
                    <!-- TOC START -->
<div id="dw__toc">
<h3 class="toggle">Table of Contents</h3>
<div>

<ul class="toc">
<li class="level1"><div class="li"><a href="#modelling">Modelling</a></div>
<ul class="toc">
<li class="level2"><div class="li"><a href="#task_1">Task 1</a></div></li>
</ul>
</li>
<li class="level1"><div class="li"><a href="#simulation">Simulation</a></div>
<ul class="toc">
<li class="level2"><div class="li"><a href="#task_2">Task 2</a></div></li>
</ul>
</li>
<li class="level1"><div class="li"><a href="#verification">Verification</a></div>
<ul class="toc">
<li class="level2"><div class="li"><a href="#task_3">Task 3</a></div></li>
</ul>
</li>
<li class="level1"><div class="li"><a href="#solutions">Solutions</a></div></li>
</ul>
</div>
</div>
<!-- TOC END -->

<h1 class="sectionedit1" id="tutorial_on_petri_nets">Tutorial on Petri nets</h1>
<div class="level1">
<div class="wrap_important plugin_wrap">
<p>
Familiarise yourself with the <a href="../../help/petri_net_plugin.html" class="wikilink1" title="help:petri_net_plugin">Petri Net plugin</a> before proceeding with this tutorial.
</p>
</div>
<p>
In this tutorial we will use the famous <a href="http://en.wikipedia.org/wiki/Dining_philosophers_problem" class="interwiki iw_wp" title="http://en.wikipedia.org/wiki/Dining_philosophers_problem">Dining philosophers problem</a> to illustrate the power and convenience of the Petri nets. The problem states that there are five philosophers sitting around a table. Each philosopher either thinks or eats. There are five forks on the table shared among philosophers in such a way that each fork can be either used by a philosopher on its left or on its right side. Before eating a philosopher tries to take both forks in some order. If a fork is already taken by a neighbouring philosopher, he will be waiting until the fork becomes available again. After eating, a philosopher returns to thinking while putting back both of his forks. 
</p>

</div>

<h2 class="sectionedit4" id="modelling">Modelling</h2>
<div class="level2">

<p>
Petri nets is an ideal tool for formally modelling the dining philosophers problem. The behaviour of a single philosopher can be modelled with <code>take_left_fork</code>, <code>put_left_fork</code>, <code>take_right_fork</code>,  <code>put_right_fork</code>, <code>start_eating</code> and <code>start_thinking</code> transitions. The state of the philosopher is captured with a token in either the <code>eating</code> or <code>thinking</code> place and the availability of forks is determined by the presence of a token in <code>fork1_free</code> and <code>fork2_free</code> places respectively (the corresponding fork is on the table), as shown in the following Petri net. 
</p>

<p>
<img src="pn-philosopher.png" class="mediacenter" alt="" />
</p>

<p>
For simplicity let us model the problem with two philosophers and two forks only. In this case, the <code>fork1_free</code> and <code>fork2_free</code> are shared by the philosophers <em>A</em> and <em>B</em> as modelled by the following Petri net.
</p>

<p>
<img src="pn-two_philosophers.png" class="mediacenter" alt="" />
</p>
<div class="wrap_box plugin_wrap">
<h3 class="sectionedit7" id="task_1">Task 1</h3>

<p>
Capture this Petri net within Workcraft. You may want to build a Petri net model of a single philosopher first, put it in a group, and then make use of copy-paste features to replicate the model for the other philosopher. Give the places and transitions some meaningful names, e.g. as in the Petri net above. As the names of places and transitions must be unique, we prepended the node names  with <em>A_</em> and <em>B_</em> prefixes to distinguish the models of philosophers <em>A</em> and <em>B</em> respectively.
</p>
</div><div class="wrap_tip plugin_wrap">
<p>
Note the difference between the names and labels:
</p>
<ul>
<li class="level1"><div class="li">
 A name is a unique alpha-numerical ID of a Petri net node which is used as the node reference in simulation and verification.
</div></li>
<li class="level1"><div class="li">
 A label is just an arbitrary text attached to a node. 
</div></li>
</ul>

</div>
</div>

<h2 class="sectionedit10" id="simulation">Simulation</h2>
<div class="level2">

<p>
Enter the simulation tool by pressing the <img src="../../help/editor_tools-simulate.png" class="media" title="[M] Simulate" alt="[M] Simulate" /> button and play with the dining philosophers model. Initially both forks are on the table and places <code>fork1_free</code> and <code>fork2_free</code> are marked. Each philosopher can take any of the forks - the corresponding <code>*_take_left_fork</code> and <code>*_take_right_fork</code> transitions are enabled for both philosophers. 
</p>

<p>
If you allow the same philosopher to take both forks (e.g., by clicking transitions <code>A_take_left_fork</code> and <code>A_take_right_fork</code>), then he can eat, while the other philosopher thinks. When he is finished with the meal he enters the thinking state (click transition <code>A_start_thinking</code>) and returns the forks (click transitions <code>A_put_left_fork</code> and <code>A_put_right_fork</code>). This trace of transitions brings us to the initial state where the philosophers compete for the forks again.
</p>

<p>
Another scenario is possible when each philosopher takes only one of the forks (e.g. click transitions <code>A_take_left_fork</code> and <code>B_take_right_fork</code>)). This leads to a deadlock as the philosophers wait for each other to return the fork, but none of them can do it until they eat.
</p>
<div class="wrap_box plugin_wrap">
<h3 class="sectionedit13" id="task_2">Task 2</h3>
<ul>
<li class="level1"><div class="li">
 Simulate the above distinctive scenarios for dining philosophers. 
</div></li>
<li class="level1"><div class="li">
 Explore the navigation buttons in the <em>Control panel</em> and go back and forth through the trace of events in your simulation. 
</div></li>
<li class="level1"><div class="li">
 Try random simulation at different animation speeds.
</div></li>
</ul>

</div>
</div>

<h2 class="sectionedit14" id="verification">Verification</h2>
<div class="level2">

<p>
Various properties of a Petri net model can be verified using <em>punf</em> and <em>mpsat</em> as the backend tools (see overview of <a href="../download/tools" class="wikilink2" title="download:tools" rel="nofollow">third-party tools</a> for more details). The tool interfaces available for Petri net verification are collected under <em>Tools→Verification</em> menu.
</p>

<p>
The easiest and most obvious property to check is that the model does not have a deadlock - choose the <em>Tools→Verification→Check for deadlocks [MPSat]</em> menu item for this. A our dining philosophers model is not deadlock-free, this should result in the following error message with a trace leading to the deadlock (you can play in the simulator by clicking the <em>Play</em> button).
</p>

<p>
<img src="deadlock_trace-two_philosophers.png" class="mediacenter" alt="" />
</p>

<p>
Verification of custom properties is based on reachability analysis on the Petri net. For this a custom property should  be expressed in <a href="../../help/reach.html" class="wikilink1" title="help:reach">Reach language</a>. For example, you can try and verify that both philosophers cannot be eating at the same time. For this you need to open <em>MPSat configuration</em> window via <em>Tools→Verification</em>, choose <em>Reachability analysis</em> as the MPSat mode, select <em>Minimise cost function</em> as the MPSat solution type, input <em>Both philosophers never eat simultaneously</em> as the property name and enter the following Reach expression in the <em>Property specification (Reach)</em> box: <code>$P“A_eating” &amp; $P“B_eating”</code>. Save this property by clicking the <em>Save as new preset…</em> button and giving it some meaningful name, e.g. <em> both_philosophers_never_eat_simultaneously</em>. Notice the space as the first symbol of the preset name - this is to have it on the top of the custom properties list that is sorted alphabetically. The result should be similar to the following screenshot.
</p>

<p>
<img src="property_check-two_philosophers-never_eat_simultaneously.png" class="mediacenter" alt="" />
</p>

<p>
Let us explain how to interpret the Reach formula. Consider an expression <code>$P“place_name”</code>. It instructs MPSat to check if a marking is reachable where the place <code>place_name</code> has a token. In basic cases one can apply logical operations and quantifiers (e.g. <code>&amp;</code>, <code>|</code>, <code>forall</code>, <code>existis</code>, etc.) to a marking which violates the property. For expressing a more sophisticated refer to <a href="../../help/reach.html" class="wikilink1" title="help:reach">Reach language documentation</a>.
</p>

<p>
In our case, the expression <code>$P“A_eating” &amp; $P“B_eating”</code> tells MPSat to check if a state is reachable where both places <code>A_eating</code> and <code>B_eating</code> are marked with tokens, which corresponds to both philosophers eating at the same time. If such a marking is reachable, then out property is violated and a trace of Petri net transitions leading to this state is reported. If this Petri net marking is not reachable, then the property is considered satisfied, as shown in the following screenshot.
</p>

<p>
<img src="property_satisfied-two_philosophers-never_eat_simultaniously.png" class="mediacenter" alt="" />
</p>
<div class="wrap_tip plugin_wrap">
<p>
Note that the Reach expression is formulated to contradict the property we want to check. If such contradiction cannot be reached, then the property we verify can never be violated, i.e. it is satisfied.
</p>
</div><div class="wrap_box plugin_wrap">
<h3 class="sectionedit19" id="task_3">Task 3</h3>
<ul>
<li class="level1"><div class="li">
 Verify the model of dining philosophers for deadlocks. Simulate the trace leading to the deadlock. 
</div></li>
<li class="level1"><div class="li">
 Modify the model in such a way that the deadlock is prevented (hint: <span class="wrap_spoiler ">force the philosophers to take the forks in particular order, one of them always takes the fork to his left first, while the other always takes the fork to his right first</span>).
</div></li>
<li class="level1"><div class="li">
 Check if any of the philosophers can be eating with one of the forks still on the table (hint: <code><span class="wrap_spoiler ">($P“A_eating” | $P“B_eating”) &amp; ($P“fork1_free” | $P“fork2_free”)</span></code>).
</div></li>
</ul>

</div>
</div>

<h2 class="sectionedit20" id="solutions">Solutions</h2>
<div class="level2">

<p>
Download all the Workcraft models discussed in this section here:
</p>

<p>
<span class="wrap_download "><a href="dining_philosophers.tar.gz" class="media mediafile mf_gz" title="tutorial:petri_net:dining_philosophers.tar.gz (14.7 KB)">Dining philosophers models</a> (14.74 KiB, <acronym title="Modified: 2014-06-20 22:28.15">4M ago</acronym>)</span>
</p>

</div>

                    <!-- wikipage stop -->
                                    </div>

                                            </div></div><!-- /content -->

            <hr class="a11y" />

            <!-- PAGE ACTIONS -->
            <div id="dokuwiki__pagetools">
                        </div>
        </div><!-- /wrapper -->

        
<!-- ********** FOOTER ********** -->
<div id="dokuwiki__footer"><div class="pad">
    
    <div class="buttons">
                <a href="http://www.dokuwiki.org/donate" title="Donate" ><img
            src="../lib/tpl/dokuwiki-light-export/images/button-donate.gif" width="80" height="15" alt="Donate" /></a>
        <a href="http://www.php.net" title="Powered by PHP" ><img
            src="../lib/tpl/dokuwiki-light-export/images/button-php.gif" width="80" height="15" alt="Powered by PHP" /></a>
        <a href="http://validator.w3.org/check/referer" title="Valid HTML5" ><img
            src="../lib/tpl/dokuwiki-light-export/images/button-html5.png" width="80" height="15" alt="Valid HTML5" /></a>
        <a href="http://jigsaw.w3.org/css-validator/check/referer?profile=css3" title="Valid CSS" ><img
            src="../lib/tpl/dokuwiki-light-export/images/button-css.png" width="80" height="15" alt="Valid CSS" /></a>
        <a href="http://dokuwiki.org/" title="Driven by DokuWiki" ><img
            src="../lib/tpl/dokuwiki-light-export/images/button-dw.png" width="80" height="15" alt="Driven by DokuWiki" /></a>
    </div>

    <div class="userInfo">
            </div>
</div></div><!-- /footer -->

    </div></div><!-- /site -->

    <div class="no"><img  width="2" height="1" alt="" /></div>
    <div id="screen__mode" class="no"></div>    <!--[if ( lte IE 7 | IE 8 ) ]></div><![endif]-->
</body>
</html>

